// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_MATH_EXPNAT_H
#define _sHT_MATH_EXPNAT_H

#include <sHT/math/vector.h>

/*@ // Exponentiation
    // Proof status: complete, automatic
    axiomatic Expnat {
      // exponentiation is repeated multiplication
      logic ℤ expnat(ℤ b, ℤ e) = product([| b |] *^ e);

      // Some disagree about this one: exp(0, 0) = 0 or 1?
      // The latter is very convenient.
      lemma expnat_empty: ∀ ℤ b; expnat(b, 0) == 1;
      lemma expnat_one: ∀ ℤ b; expnat(b, 1) == b;

      // Actually belongs to Frama-C's bag of lemmas
      lemma expnat_split_help: ∀ ℤ b, e0, e1; e0 >= 0 && e1 >= 0
        ==> [| b |] *^ (e0 + e1) == ([| b |] *^ e0 ^ [| b |] *^ e1);
      lemma expnat_split: ∀ ℤ b, e0, e1; e0 >= 0 && e1 >= 0
        ==> expnat(b, e0 + e1) == expnat(b, e0) * expnat(b, e1);
      lemma expnat_ind: ∀ ℤ b, e; b >= 0 && e >= 0 ==> b * expnat(b, e) == expnat(b, e + 1);
    } */

/*@ // Title: Element-wise exponentiation in ℤ
    // Note(Usage, Axiom): can be eliminated once lambdas are supported
    // Proof status: incomplete, automatic
    axiomatic IotaExpnat {
      // (2, 5) ==> [| 16, 8, 4, 2, 1 |]
      logic \list<ℤ> exp_countdown(ℤ b, ℤ n);

      axiom exp_countdown_length: ∀ ℤ b, n; 0 <= n
        ==> \length(exp_countdown(b, n)) == n;
      axiom exp_countdown_at: ∀ ℤ b, n, i; 0 <= i < n
        ==> \nth(exp_countdown(b, n), i) == expnat(b, n - i - 1);

      // A check
      lemma exp_countdown_last: ∀ ℤ b, n; 0 < n
        ==> \nth(exp_countdown(b, n), n - 1) == 1;
    } */

#endif
